T:Type, p:FinProbSpace, l:IdLnk, ds:x:Id fp Type, P:(State(ds)), f:(State(ds)OutcomeT).
Normal(T)
 Normal(ds)
 (at src(l):action a(m) precondition P sends [tg,f] on link l  Realizer) 

latex

Definitions

at src(l):action $a(m) precondition P sends [$tg,f] on link l, xdom(f). v=f(x)   P(x;v), b, Rpre(loc;ds;a;p;P), source(l), Rsends(ds;knd;T;l;dt;g), <a, b>, x.A(x), f(a), IdDeq, DeclaredType(ds;x), x : v, Rsframe(lnk;tag;L), [car / cdr], locl(a), Knd, [], Realizer, "$x", Top, x:A.B(x), Normal(ds), Normal(T), Outcome, a:A fp B(a), State(ds), , IdLnk, FinProbSpace, Id, type List, x:A  B(x), s = t, a  j < b. E(j), l[i], xL. P(x), x. t(x), r  s, #$n, (x  l), , x:A. B(x), x:AB(x), Void, {i..j}, {x:A| B(x)} , , i  j < k, A  B, P & Q, A, False, P  Q, a < b, ||as||, t  T, Type

Lemmas

l member wf, int inc rationals, qle wf, l all wf2, int seg wf, select wf, length wf1, qsum wf, rationals wf, Id wf, bool wf, decl-state wf, p-outcome wf, normal-type wf, normal-ds wf, es realizer wf, Knd wf, locl wf, Rsframe wf, fpf-single wf, decl-type wf, id-deq wf, fpf-cap-single1, Rsends wf, lsrc wf, Rpre wf, Rlist wf